<!DOCTYPE html>
<!--
     SPDX-License-Identifier: CC-BY-SA-4.0
     SPDX-FileCopyrightText: 2020 seL4 Project a Series of LF Projects, LLC.
-->
<!-- Page last generated 2025-02-20 03:16:15 +0000 -->
<html lang="en">
  <head>
    <meta charset="utf-8">
    <meta http-equiv="X-UA-Compatible" content="IE=edge">
    <meta name="viewport" content="width=device-width, initial-scale=1">
    <title>Verified Configurations | seL4 docs</title>

    <!-- Our stylesheet and theme stylesheet.  Contains bootstrap. -->
    <link rel="stylesheet" href="/assets/css/style.css" type="text/css">
    <!-- Font awesome -->
    <link href="https://use.fontawesome.com/releases/v5.0.8/css/all.css" rel="stylesheet">
    <link href="https://fonts.googleapis.com/css2?family=Roboto&display=swap" rel="stylesheet">
    <!-- Pygments syntax highlighting  -->
    <link rel="stylesheet" href="/assets/css/highlighting/trac.css" type="text/css">
    <link rel="icon" type="image/x-icon" href="/assets/favicon.ico"><script defer data-domain="docs.sel4.systems"
	    src="https://analytics.sel4.systems/js/script.js"></script></head>

  <body class="container-fluid">

    



<header>
  <ul class="row menu">
    <li class="col-xs-12 col-md-2" >
            <a href="https://sel4.systems" class="skip-icon">
              <img class="img-responsive" src="/assets/logo-text-white.svg" alt="seL4 logo" />
            </a>
    </li>
    <li class="col-xs-12 col-md-10 menu">
      <nav aria-label="Banner links">
        <h2><a href="/Resources" />Resources</h2>
        <h2><a href="/processes" />Contributing</a></h2>
        <h2><a href="/projects" />Projects</h2>
        <h2><a href="/Tutorials" />Tutorials</h2>
        <iframe title="DuckDuckGo search bar" src="https://duckduckgo.com/search.html?site=docs.sel4.systems&prefill=Search%20sel4.systems" style="overflow:hidden;margin-bottom:10px; padding:0;height:40px;float:right;border-width: 0px"></iframe>
      </nav>
    </li>
  </ul>
  <div class="clear"></div>
  
<div class="breadcrumbs bootstrap hidden-sm-down">
  <nav class="sel-breadcrumb" aria-label="Breadcrumb" >
    <ol class=" list-unstyled" vocab="http://schema.org/" typeof="BreadcrumbList">
      
      
        

        

        <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <a property="item" typeof="WebPage" href="/">
              <span property="name"><b>seL4 Docs</b></span>
            </a>
            <meta property="position" content="1" />
        </li>
      
        

        

        <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <a property="item" typeof="WebPage" href="/projects/">
              <span property="name"><b>Projects</b></span>
            </a>
            <meta property="position" content="2" />
        </li>
      
        

        

        <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <a property="item" typeof="WebPage" href="/projects/sel4/">
              <span property="name"><b>The seL4 microkernel</b></span>
            </a>
            <meta property="position" content="3" />
        </li>
      
        

        
          <li class="breadcrumb-item" property="itemListElement" typeof="ListItem">
            <span property="name">Verified Configurations</span>
            <meta property="position" content="4" /></li>
          
    </ol>
  </nav>
  <nav class="sel-version" aria-label="Current Versions">
    <ol class="list-unstyled">
      <li class="list-unstyled text-right" style="margin-left:auto; padding:0rem 0rem;">
        Current versions:</li>
      <li class="list-unstyled text-right">
      <a href="/releases/sel4/13.0.0"><b>seL4-13.0.0</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/microkit/1.4.1"><b>microkit-1.4.1</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/camkes/camkes-3.11.0"><b>camkes-3.11.0</b></a></li>
      <li class="list-unstyled text-right">
      <a href="/releases/capdl/0.3.0"><b>capDL-0.3.0</b></a></li>
      </ol>
  </nav>
  <div class='clear'></div>
</div>


</header>

    <main>
      <div class="row">
  <div class="hidden-xs col-sm-4 col-md-3 col-lg-2">
    


<div class="sidebar">



      <ul class="nav nav-sidebar">
  
        <li class="">
          <a class="" href="/Resources.html">
            Resources
          </a>
        </li>
  
        <li class="">
          <a class="" href="/projects/sel4/documentation.html">
            seL4 Documentation
          </a>
        </li>
  
        <li class="">
          <a class="" href="/projects/sel4/frequently-asked-questions.html">
            seL4 FAQ
          </a>
        </li>
  
        <li class="">
          <a class="" href="/projects/buildsystem/host-dependencies.html">
            Set up your machine
          </a>
        </li>
  
        <li class="">
          <a class="" href="/Hardware/">
            Supported platforms
          </a>
        </li>
  
        <li class="">
          <a class="" href="/projects/available-user-components.html">
            Available components
          </a>
        </li>
  
        <li class="">
          <a class="" href="/projects/roadmap.html">
            Roadmap
          </a>
        </li>
  
        <li class="">
          <a class="" href="/CommunityProjects.html">
            Community projects
          </a>
        </li>
  
        <li class="">
          <a class="" href="/releases/sel4">
            Release Notes
          </a>
        </li>
  
        <li class="">
          <a class="" href="/projects/sel4/api-doc.html">
            libsel4 API
          </a>
        </li>
  
        <li class="">
          <a class="" href="https://sel4.systems/Info/Docs/seL4-manual-latest.pdf">
            Current Manual
          </a>
        </li>
  
        <li class="active">
          <a class="" href="/projects/sel4/verified-configurations.html">
            Verified Configurations
          </a>
        </li>
  
      </ul>














</div>

  </div>
  <div class="content col-sm-8 col-md-6 col-lg-7 main">
    <h1 id="verified-configurations">Verified Configurations</h1>

<p>This page describes which architecture/platform/configuration
combinations of seL4 have verified properties, which configurations
possess which properties, and how to obtain an seL4 version for a
specified configuration.</p>

<p>At this time, verification of seL4 remains a more time-intensive process
than software development. Consequently, while seL4 has been ported to
multiple architectures, and its build system allows further
configuration of internal and hardware features, verified configurations
are necessarily both less numerous and more specific.</p>

<p>These configurations are also referred to as <em>verification platforms</em>,
currently constituting: ARM, ARM_HYP, ARM_MCS, AARCH64, RISCV64, RISCV64_MCS, X64</p>

<p>Please consult <a href="/FrequentlyAskedQuestions">Frequently Asked
Questions</a>, as well as the <a href="http://sel4.systems/Info/FAQ/proof.html">proof and
assumptions page</a> for a better
understanding of the intersection of verification and seL4.</p>

<h2 id="examining-and-building-verified-configurations">Examining and Building Verified Configurations</h2>

<p>Current verified configurations can be found in seL4 sources in the
<code class="language-plaintext highlighter-rouge">configs</code> folder:</p>
<div class="language-sh highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="nb">cd </span>configs/
<span class="nb">ls</span> <span class="k">*</span>_verified.cmake
<span class="c"># AARCH64_bcm2711_verified.cmake    ARM_exynos5410_verified.cmake</span>
<span class="c"># AARCH64_hikey_verified.cmake      ARM_exynos5422_verified.cmake</span>
<span class="c"># AARCH64_odroidc2_verified.cmake   ARM_hikey_verified.cmake</span>
<span class="c"># AARCH64_odroidc4_verified.cmake   ARM_imx8mm_verified.cmake</span>
<span class="c"># AARCH64_verified.cmake            ARM_tk1_verified.cmake</span>
<span class="c"># AARCH64_zynqmp_verified.cmake     ARM_verified.cmake</span>
<span class="c"># ARM_HYP_exynos5410_verified.cmake ARM_zynq7000_verified.cmake</span>
<span class="c"># ARM_HYP_exynos5_verified.cmake    ARM_zynqmp_verified.cmake</span>
<span class="c"># ARM_HYP_verified.cmake            RISCV64_MCS_verified.cmake</span>
<span class="c"># ARM_MCS_verified.cmake            RISCV64_verified.cmake</span>
<span class="c"># ARM_exynos4_verified.cmake        X64_verified.cmake</span>
</code></pre></div></div>

<p>To obtain specific source code and build for a given configuration (e.g.
ARM) in a build directory:</p>
<div class="language-sh highlighter-rouge"><div class="highlight"><pre class="highlight"><code><span class="nb">mkdir </span>build
<span class="nb">cd </span>build
cmake <span class="nt">-P</span> ../config/ARM_verified.cmake
</code></pre></div></div>

<p>Notably <code class="language-plaintext highlighter-rouge">kernel.elf</code> is the kernel binary, and <code class="language-plaintext highlighter-rouge">kernel_all_pp.c</code> is
the kernel source code after preprocessing, which is used as the basis
for verification efforts.</p>

<p>Also see <a href="/Developing/Building/seL4Standalone">Stand-alone seL4 builds</a>
for general guidelines on generating an seL4 binary from an existing
configuration and what to do with a <code class="language-plaintext highlighter-rouge">kernel.elf</code> file.</p>

<h2 id="available-verified-configurations">Available Verified Configurations</h2>

<h3 id="unverified-features">Unverified Features</h3>

<p>At present, none of our verified configurations take into account
address translation for devices (System MMU or IOMMU), debug/profiling
interfaces, or the kernel startup at boot.</p>

<p>The proofs for RISCV64_MCS/ARM_MCS (mixed-criticality extensions to real-time
seL4 features), as well as security proofs for AARCH64 are in progress. Refer to
the <a href="/projects/roadmap.html">roadmap</a> for status and upcoming features.</p>

<h2 id="arm-sabre-lite">ARM Sabre Lite</h2>

<table>
  <tbody>
    <tr>
      <td>File</td>
      <td><code class="language-plaintext highlighter-rouge">ARM_verified.cmake</code></td>
    </tr>
    <tr>
      <td>Architecture</td>
      <td>ARMv7, 32 bit</td>
    </tr>
    <tr>
      <td>Platform</td>
      <td>i.MX 6 (Sabre Lite)</td>
    </tr>
    <tr>
      <td>Floating-point support</td>
      <td>No</td>
    </tr>
    <tr>
      <td>Hypervisor mode</td>
      <td>No</td>
    </tr>
    <tr>
      <td><strong>Verified properties</strong></td>
      <td>functional correctness incl fast path, integrity (access control), confidentiality (information flow), binary correctness (covers all verified C code), user-level system initialisation</td>
    </tr>
  </tbody>
</table>

<h2 id="exynos4">ARM Exynos 4</h2>

<table>
  <tbody>
    <tr>
      <td>File</td>
      <td><code class="language-plaintext highlighter-rouge">ARM_exynos4_verified.cmake</code></td>
    </tr>
    <tr>
      <td>Architecture</td>
      <td>ARMv7, 32 bit</td>
    </tr>
    <tr>
      <td>Platform</td>
      <td>exynos4</td>
    </tr>
    <tr>
      <td>Floating-point support</td>
      <td>No</td>
    </tr>
    <tr>
      <td>Hypervisor mode</td>
      <td>No</td>
    </tr>
    <tr>
      <td><strong>Verified properties</strong></td>
      <td>functional correctness incl fast path, integrity (access control), confidentiality (information flow), binary correctness (covers all verified C code), user-level system initialisation</td>
    </tr>
  </tbody>
</table>

<h2 id="arm-exynos-5">ARM Exynos 5</h2>

<table>
  <tbody>
    <tr>
      <td>File</td>
      <td><code class="language-plaintext highlighter-rouge">ARM_exynos5410_verified.cmake</code> and <code class="language-plaintext highlighter-rouge">ARM_exynos5422_verified.cmake</code></td>
    </tr>
    <tr>
      <td>Architecture</td>
      <td>ARMv7, 32 bit</td>
    </tr>
    <tr>
      <td>Platform</td>
      <td>exynos5410 and exynos5422</td>
    </tr>
    <tr>
      <td>Floating-point support</td>
      <td>No</td>
    </tr>
    <tr>
      <td>Hypervisor mode</td>
      <td>No</td>
    </tr>
    <tr>
      <td><strong>Verified properties</strong></td>
      <td>functional correctness incl fast path, integrity (access control), confidentiality (information flow), binary correctness (covers all verified C code), user-level system initialisation</td>
    </tr>
  </tbody>
</table>

<h2 id="arm-hikey">ARM Hikey</h2>

<table>
  <tbody>
    <tr>
      <td>File</td>
      <td><code class="language-plaintext highlighter-rouge">ARM_hikey_verified.cmake</code></td>
    </tr>
    <tr>
      <td>Architecture</td>
      <td>ARMv7, 32 bit</td>
    </tr>
    <tr>
      <td>Platform</td>
      <td>hikey</td>
    </tr>
    <tr>
      <td>Floating-point support</td>
      <td>No</td>
    </tr>
    <tr>
      <td>Hypervisor mode</td>
      <td>No</td>
    </tr>
    <tr>
      <td><strong>Verified properties</strong></td>
      <td>functional correctness incl fast path, integrity (access control), confidentiality (information flow), binary correctness (covers all verified C code), user-level system initialisation</td>
    </tr>
  </tbody>
</table>

<h2 id="tk1">ARM TK1</h2>

<table>
  <tbody>
    <tr>
      <td>File</td>
      <td><code class="language-plaintext highlighter-rouge">ARM_tk1_verified.cmake</code></td>
    </tr>
    <tr>
      <td>Architecture</td>
      <td>ARMv7, 32 bit</td>
    </tr>
    <tr>
      <td>Platform</td>
      <td>Jetson TK1</td>
    </tr>
    <tr>
      <td>Floating-point support</td>
      <td>No</td>
    </tr>
    <tr>
      <td>Hypervisor mode</td>
      <td>No</td>
    </tr>
    <tr>
      <td><strong>Verified properties</strong></td>
      <td>functional correctness incl fast path, integrity (access control), confidentiality (information flow), binary correctness (covers all verified C code), user-level system initialisation</td>
    </tr>
  </tbody>
</table>

<h2 id="zynq7000">ARM Zynq7000</h2>

<table>
  <tbody>
    <tr>
      <td>File</td>
      <td><code class="language-plaintext highlighter-rouge">ARM_zynq7000_verified.cmake</code></td>
    </tr>
    <tr>
      <td>Architecture</td>
      <td>ARMv7, 32 bit</td>
    </tr>
    <tr>
      <td>Platform</td>
      <td>zynq7000</td>
    </tr>
    <tr>
      <td>Floating-point support</td>
      <td>No</td>
    </tr>
    <tr>
      <td>Hypervisor mode</td>
      <td>No</td>
    </tr>
    <tr>
      <td><strong>Verified properties</strong></td>
      <td>functional correctness incl fast path, integrity (access control), confidentiality (information flow), binary correctness (covers all verified C code), user-level system initialisation</td>
    </tr>
  </tbody>
</table>

<h2 id="arm-zynqmp">ARM ZynqMP</h2>

<table>
  <tbody>
    <tr>
      <td>File</td>
      <td><code class="language-plaintext highlighter-rouge">ARM_zynqmp_verified.cmake</code></td>
    </tr>
    <tr>
      <td>Architecture</td>
      <td>ARMv7, 32 bit</td>
    </tr>
    <tr>
      <td>Platform</td>
      <td>zcu102 and zcu106 in 32 bit mode</td>
    </tr>
    <tr>
      <td>Floating-point support</td>
      <td>No</td>
    </tr>
    <tr>
      <td>Hypervisor mode</td>
      <td>No</td>
    </tr>
    <tr>
      <td><strong>Verified properties</strong></td>
      <td>functional correctness incl fast path, integrity (access control), confidentiality (information flow), binary correctness (covers all verified C code), user-level system initialisation</td>
    </tr>
  </tbody>
</table>

<h2 id="imx8mm">ARM IMX8MM-EVK</h2>

<table>
  <tbody>
    <tr>
      <td>File</td>
      <td><code class="language-plaintext highlighter-rouge">ARM_imx8mm_verified.cmake</code></td>
    </tr>
    <tr>
      <td>Architecture</td>
      <td>ARMv7, 32 bit</td>
    </tr>
    <tr>
      <td>Platform</td>
      <td>IMX8MM-EVK</td>
    </tr>
    <tr>
      <td>Floating-point support</td>
      <td>Yes</td>
    </tr>
    <tr>
      <td>Hypervisor mode</td>
      <td>No</td>
    </tr>
    <tr>
      <td><strong>Verified properties</strong></td>
      <td>functional correctness incl fast path</td>
    </tr>
  </tbody>
</table>

<h2 id="arm_hyp-tk1">ARM_HYP TK1</h2>

<table>
  <tbody>
    <tr>
      <td>File</td>
      <td><code class="language-plaintext highlighter-rouge">ARM_HYP_verified.cmake</code></td>
    </tr>
    <tr>
      <td>Architecture</td>
      <td>ARMv7, 32 bit</td>
    </tr>
    <tr>
      <td>Platform</td>
      <td>Tegra TK1</td>
    </tr>
    <tr>
      <td>Floating-point support</td>
      <td>No</td>
    </tr>
    <tr>
      <td>Hypervisor mode</td>
      <td>Yes</td>
    </tr>
    <tr>
      <td><strong>Verified properties</strong></td>
      <td>functional correctness, incl fast path</td>
    </tr>
  </tbody>
</table>

<h2 id="arm_hyp-exynos5">ARM_HYP Exynos5</h2>

<table>
  <tbody>
    <tr>
      <td>File</td>
      <td><code class="language-plaintext highlighter-rouge">ARM_HYP_exynos5_verified.cmake</code> and <code class="language-plaintext highlighter-rouge">ARM_HYP_exynos5410_verified.cmake</code></td>
    </tr>
    <tr>
      <td>Architecture</td>
      <td>ARMv7, 32 bit</td>
    </tr>
    <tr>
      <td>Platform</td>
      <td>Odroid XU4</td>
    </tr>
    <tr>
      <td>Floating-point support</td>
      <td>No</td>
    </tr>
    <tr>
      <td>Hypervisor mode</td>
      <td>Yes</td>
    </tr>
    <tr>
      <td><strong>Verified properties</strong></td>
      <td>functional correctness, incl fast path</td>
    </tr>
  </tbody>
</table>

<h2 id="arm_mcs">ARM_MCS</h2>

<table>
  <tbody>
    <tr>
      <td>File</td>
      <td><code class="language-plaintext highlighter-rouge">ARM_MCS_verified.cmake</code></td>
    </tr>
    <tr>
      <td>Architecture</td>
      <td>ARMv7, 32 bit</td>
    </tr>
    <tr>
      <td>Platform</td>
      <td>i.MX 6 (Sabre Lite)</td>
    </tr>
    <tr>
      <td>Floating-point support</td>
      <td>No</td>
    </tr>
    <tr>
      <td>Hypervisor mode</td>
      <td>No</td>
    </tr>
    <tr>
      <td>Mixed-Criticality-Systems API</td>
      <td>Yes</td>
    </tr>
    <tr>
      <td><strong>Verified properties</strong></td>
      <td>in progress (design-level functional correctness completed)</td>
    </tr>
  </tbody>
</table>

<h2 id="aarch64">AARCH64</h2>

<table>
  <tbody>
    <tr>
      <td>File</td>
      <td><code class="language-plaintext highlighter-rouge">AARCH64_verified.cmake</code></td>
    </tr>
    <tr>
      <td>Architecture</td>
      <td>ARMv8, 64 bit</td>
    </tr>
    <tr>
      <td>Platform</td>
      <td>Tegra X2 (Jetson TX2)</td>
    </tr>
    <tr>
      <td>Floating-point support</td>
      <td>Yes</td>
    </tr>
    <tr>
      <td>Hypervisor mode</td>
      <td>Yes</td>
    </tr>
    <tr>
      <td><strong>Verified properties</strong></td>
      <td>functional correctness, incl fast path completed; integrity proof in progress</td>
    </tr>
  </tbody>
</table>

<h2 id="bcm2711">AARCH64 RPI4</h2>

<table>
  <tbody>
    <tr>
      <td>File</td>
      <td><code class="language-plaintext highlighter-rouge">AARCH64_bcm2711_verified.cmake</code></td>
    </tr>
    <tr>
      <td>Architecture</td>
      <td>ARMv8, 64 bit</td>
    </tr>
    <tr>
      <td>Platform</td>
      <td>bcm2711 (Raspberry PI 4)</td>
    </tr>
    <tr>
      <td>Floating-point support</td>
      <td>Yes</td>
    </tr>
    <tr>
      <td>Hypervisor mode</td>
      <td>Yes</td>
    </tr>
    <tr>
      <td><strong>Verified properties</strong></td>
      <td>functional correctness, incl fast path completed; integrity proof in progress</td>
    </tr>
  </tbody>
</table>

<h2 id="hikey">AARCH64 Hikey</h2>

<table>
  <tbody>
    <tr>
      <td>File</td>
      <td><code class="language-plaintext highlighter-rouge">AARCH64_hikey_verified.cmake</code></td>
    </tr>
    <tr>
      <td>Architecture</td>
      <td>ARMv8, 64 bit</td>
    </tr>
    <tr>
      <td>Platform</td>
      <td>hikey</td>
    </tr>
    <tr>
      <td>Floating-point support</td>
      <td>Yes</td>
    </tr>
    <tr>
      <td>Hypervisor mode</td>
      <td>Yes</td>
    </tr>
    <tr>
      <td><strong>Verified properties</strong></td>
      <td>functional correctness, incl fast path completed; integrity proof in progress</td>
    </tr>
  </tbody>
</table>

<h2 id="odroidc2">AARCH64 Odroid C2</h2>

<table>
  <tbody>
    <tr>
      <td>File</td>
      <td><code class="language-plaintext highlighter-rouge">AARCH64_odroidc2_verified.cmake</code></td>
    </tr>
    <tr>
      <td>Architecture</td>
      <td>ARMv8, 64 bit</td>
    </tr>
    <tr>
      <td>Platform</td>
      <td>odroidc2</td>
    </tr>
    <tr>
      <td>Floating-point support</td>
      <td>Yes</td>
    </tr>
    <tr>
      <td>Hypervisor mode</td>
      <td>Yes</td>
    </tr>
    <tr>
      <td><strong>Verified properties</strong></td>
      <td>functional correctness, incl fast path completed; integrity proof in progress</td>
    </tr>
  </tbody>
</table>

<h2 id="odroidc4">AARCH64 Odroid C4</h2>

<table>
  <tbody>
    <tr>
      <td>File</td>
      <td><code class="language-plaintext highlighter-rouge">AARCH64_odroidc4_verified.cmake</code></td>
    </tr>
    <tr>
      <td>Architecture</td>
      <td>ARMv8, 64 bit</td>
    </tr>
    <tr>
      <td>Platform</td>
      <td>odroidc4</td>
    </tr>
    <tr>
      <td>Floating-point support</td>
      <td>Yes</td>
    </tr>
    <tr>
      <td>Hypervisor mode</td>
      <td>Yes</td>
    </tr>
    <tr>
      <td><strong>Verified properties</strong></td>
      <td>functional correctness, incl fast path completed; integrity proof in progress</td>
    </tr>
  </tbody>
</table>

<h2 id="zynqmp">AARCH64 ZynqMP</h2>

<table>
  <tbody>
    <tr>
      <td>File</td>
      <td><code class="language-plaintext highlighter-rouge">AARCH64_zynqmp_verified.cmake</code></td>
    </tr>
    <tr>
      <td>Architecture</td>
      <td>ARMv8, 64 bit</td>
    </tr>
    <tr>
      <td>Platform</td>
      <td>zynqmp (zcu102 and zcu106)</td>
    </tr>
    <tr>
      <td>Floating-point support</td>
      <td>Yes</td>
    </tr>
    <tr>
      <td>Hypervisor mode</td>
      <td>Yes</td>
    </tr>
    <tr>
      <td><strong>Verified properties</strong></td>
      <td>functional correctness, incl fast path completed; integrity proof in progress</td>
    </tr>
  </tbody>
</table>

<h2 id="riscv64">RISCV64</h2>

<table>
  <tbody>
    <tr>
      <td>File</td>
      <td><code class="language-plaintext highlighter-rouge">RISCV64_verified.cmake</code></td>
    </tr>
    <tr>
      <td>Architecture</td>
      <td>RISC-V 64-bit</td>
    </tr>
    <tr>
      <td>Platform</td>
      <td>HiFive</td>
    </tr>
    <tr>
      <td>Floating-point support</td>
      <td>No</td>
    </tr>
    <tr>
      <td>Hypervisor mode</td>
      <td>No</td>
    </tr>
    <tr>
      <td><strong>Verified properties</strong></td>
      <td>functional correctness, integrity (access control), confidentiality (information flow); verification of fast path in progress</td>
    </tr>
  </tbody>
</table>

<h2 id="riscv64_mcs">RISCV64_MCS</h2>

<table>
  <tbody>
    <tr>
      <td>File</td>
      <td><code class="language-plaintext highlighter-rouge">RISCV64_MCS_verified.cmake</code></td>
    </tr>
    <tr>
      <td>Architecture</td>
      <td>RISC-V 64-bit</td>
    </tr>
    <tr>
      <td>Platform</td>
      <td>HiFive</td>
    </tr>
    <tr>
      <td>Floating-point support</td>
      <td>No</td>
    </tr>
    <tr>
      <td>Hypervisor mode</td>
      <td>No</td>
    </tr>
    <tr>
      <td>Mixed-Criticality-Systems API</td>
      <td>Yes</td>
    </tr>
    <tr>
      <td><strong>Verified properties</strong></td>
      <td>C verification in progress (design-level functional correctness completed)</td>
    </tr>
  </tbody>
</table>

<h2 id="x64">X64</h2>

<table>
  <tbody>
    <tr>
      <td>File</td>
      <td><code class="language-plaintext highlighter-rouge">X64_verified.cmake</code></td>
    </tr>
    <tr>
      <td>Architecture/Platform</td>
      <td>x86 64-bit</td>
    </tr>
    <tr>
      <td>Floating-point support</td>
      <td>Yes</td>
    </tr>
    <tr>
      <td>Hypervisor mode</td>
      <td>No</td>
    </tr>
    <tr>
      <td><strong>Verified properties</strong></td>
      <td>functional correctness, no fast path</td>
    </tr>
  </tbody>
</table>

  </div>







  
    
<div class="sidebar-toc hidden-xs hidden-sm col-md-3 col-lg-3">
    <ul id="toc" class="section-nav">
<li class="toc-entry toc-h2"><a href="#examining-and-building-verified-configurations">Examining and Building Verified Configurations</a></li>
<li class="toc-entry toc-h2"><a href="#available-verified-configurations">Available Verified Configurations</a>
<ul>
<li class="toc-entry toc-h3"><a href="#unverified-features">Unverified Features</a></li>
</ul>
</li>
<li class="toc-entry toc-h2"><a href="#arm-sabre-lite">ARM Sabre Lite</a></li>
<li class="toc-entry toc-h2"><a href="#exynos4">ARM Exynos 4</a></li>
<li class="toc-entry toc-h2"><a href="#arm-exynos-5">ARM Exynos 5</a></li>
<li class="toc-entry toc-h2"><a href="#arm-hikey">ARM Hikey</a></li>
<li class="toc-entry toc-h2"><a href="#tk1">ARM TK1</a></li>
<li class="toc-entry toc-h2"><a href="#zynq7000">ARM Zynq7000</a></li>
<li class="toc-entry toc-h2"><a href="#arm-zynqmp">ARM ZynqMP</a></li>
<li class="toc-entry toc-h2"><a href="#imx8mm">ARM IMX8MM-EVK</a></li>
<li class="toc-entry toc-h2"><a href="#arm_hyp-tk1">ARM_HYP TK1</a></li>
<li class="toc-entry toc-h2"><a href="#arm_hyp-exynos5">ARM_HYP Exynos5</a></li>
<li class="toc-entry toc-h2"><a href="#arm_mcs">ARM_MCS</a></li>
<li class="toc-entry toc-h2"><a href="#aarch64">AARCH64</a></li>
<li class="toc-entry toc-h2"><a href="#bcm2711">AARCH64 RPI4</a></li>
<li class="toc-entry toc-h2"><a href="#hikey">AARCH64 Hikey</a></li>
<li class="toc-entry toc-h2"><a href="#odroidc2">AARCH64 Odroid C2</a></li>
<li class="toc-entry toc-h2"><a href="#odroidc4">AARCH64 Odroid C4</a></li>
<li class="toc-entry toc-h2"><a href="#zynqmp">AARCH64 ZynqMP</a></li>
<li class="toc-entry toc-h2"><a href="#riscv64">RISCV64</a></li>
<li class="toc-entry toc-h2"><a href="#riscv64_mcs">RISCV64_MCS</a></li>
<li class="toc-entry toc-h2"><a href="#x64">X64</a></li>
</ul>
</div>

  
  
<div class="sidebar-toc hidden-xs hidden-sm col-md-3 col-lg-3">
  
    <ul class="section-nav">
    	<h2> seL4 </h2> 
        <li>
          
          <a style="" class="" href="/projects/sel4/">
            Documentation homepage
          </a>
        </li>




        <li>
          
          <a style="" class="" href="/projects/sel4/status.html">
            Status
          </a>
        </li>














    
        <h3>Repositories</h3>
    
        <li>
          <a class="" href="https://github.com/seL4/sel4">
            sel4
          </a>
        </li>









<h3>Releases</h3>

    
      <li>
        <a style="" href="/releases/sel4/13.0.0.html">
          seL4 13.0.0
        </a> (<a style="" href="http://sel4.systems/Info/Docs/seL4-manual-13.0.0.pdf">manual</a>)
      </li>

    


    
      <li>
        <a style="" href="/releases/sel4/12.1.0.html">
          seL4 12.1.0
        </a> (<a style="" href="http://sel4.systems/Info/Docs/seL4-manual-12.1.0.pdf">manual</a>)
      </li>

    


    
      <li>
        <a style="" href="/releases/sel4/12.0.0.html">
          seL4 12.0.0
        </a> (<a style="" href="http://sel4.systems/Info/Docs/seL4-manual-12.0.0.pdf">manual</a>)
      </li>

    


    
      <li>
        <a style="" href="/releases/sel4/11.0.0.html">
          seL4 11.0.0
        </a> (<a style="" href="http://sel4.systems/Info/Docs/seL4-manual-11.0.0.pdf">manual</a>)
      </li>

    


    


    
      <li>
        <a style="" href="/releases/sel4/10.1.1.html">
          seL4 10.1.1
        </a> (<a style="" href="http://sel4.systems/Info/Docs/seL4-manual-10.1.1.pdf">manual</a>)
      </li>

    


    
      <li>
        <a style="" href="/releases/sel4/10.1.0.html">
          seL4 10.1.0
        </a> (<a style="" href="http://sel4.systems/Info/Docs/seL4-manual-10.1.0.pdf">manual</a>)
      </li>

    


    
      <li>
        <a style="" href="/releases/sel4/10.0.0.html">
          seL4 10.0.0
        </a> (<a style="" href="http://sel4.systems/Info/Docs/seL4-manual-10.0.0.pdf">manual</a>)
      </li>

    


    
      <li>
        <a style="" href="/releases/sel4/9.0.1.html">
          seL4 9.0.1
        </a> (<a style="" href="http://sel4.systems/Info/Docs/seL4-manual-9.0.1.pdf">manual</a>)
      </li>

    


    


    
      <li>
        <a style="" href="/releases/sel4/9.0.0.html">
          seL4 9.0.0
        </a> (<a style="" href="http://sel4.systems/Info/Docs/seL4-manual-9.0.0.pdf">manual</a>)
      </li>

    


    
      <li>
        <a style="" href="/releases/sel4/8.0.0.html">
          seL4 8.0.0
        </a> (<a style="" href="http://sel4.systems/Info/Docs/seL4-manual-8.0.0.pdf">manual</a>)
      </li>

    


    
      <li>
        <a style="" href="/releases/sel4/7.0.0.html">
          seL4 7.0.0
        </a> (<a style="" href="http://sel4.systems/Info/Docs/seL4-manual-7.0.0.pdf">manual</a>)
      </li>

    


    
      <li>
        <a style="" href="/releases/sel4/6.0.0.html">
          seL4 6.0.0
        </a> (<a style="" href="http://sel4.systems/Info/Docs/seL4-manual-6.0.0.pdf">manual</a>)
      </li>

    


    


    
      <li>
        <a style="" href="/releases/sel4/5.2.0.html">
          seL4 5.2.0
        </a> (<a style="" href="http://sel4.systems/Info/Docs/seL4-manual-5.2.0.pdf">manual</a>)
      </li>

    


    
      <li>
        <a style="" href="/releases/sel4/5.1.0.html">
          seL4 5.1.0
        </a> (<a style="" href="http://sel4.systems/Info/Docs/seL4-manual-5.1.0.pdf">manual</a>)
      </li>

    


    
      <li>
        <a style="" href="/releases/sel4/5.0.0.html">
          seL4 5.0.0
        </a> (<a style="" href="http://sel4.systems/Info/Docs/seL4-manual-5.0.0.pdf">manual</a>)
      </li>

    


    
      <li>
        <a style="" href="/releases/sel4/4.0.0.html">
          seL4 4.0.0
        </a> (<a style="" href="http://sel4.systems/Info/Docs/seL4-manual-4.0.0.pdf">manual</a>)
      </li>

    


    
      <li>
        <a style="" href="/releases/sel4/3.2.0.html">
          seL4 3.2.0
        </a> (<a style="" href="http://sel4.systems/Info/Docs/seL4-manual-3.2.0.pdf">manual</a>)
      </li>

    


    
      <li>
        <a style="" href="/releases/sel4/3.1.0.html">
          seL4 3.1.0
        </a> (<a style="" href="http://sel4.systems/Info/Docs/seL4-manual-3.1.0.pdf">manual</a>)
      </li>

    


    
      <li>
        <a style="" href="/releases/sel4/3.0.1.html">
          seL4 3.0.1
        </a> (<a style="" href="http://sel4.systems/Info/Docs/seL4-manual-3.0.1.pdf">manual</a>)
      </li>

    


    
      <li>
        <a style="" href="/releases/sel4/3.0.0.html">
          seL4 3.0.0
        </a> (<a style="" href="http://sel4.systems/Info/Docs/seL4-manual-3.0.0.pdf">manual</a>)
      </li>

    


    
      <li>
        <a style="" href="/releases/sel4/2.1.0.html">
          seL4 2.1.0
        </a> (<a style="" href="http://sel4.systems/Info/Docs/seL4-manual-2.1.0.pdf">manual</a>)
      </li>

    


    
      <li>
        <a style="" href="/releases/sel4/2.0.0.html">
          seL4 2.0.0
        </a> (<a style="" href="http://sel4.systems/Info/Docs/seL4-manual-2.0.0.pdf">manual</a>)
      </li>

    


    


    










    </ul>

</div>


</div>

    </main>
    


<footer class="site-footer">

  <h2 class="footer-heading">seL4 docs</h2>

  <div class="footer-col-wrapper">

    <div class="col-md-2">
      



<ul class="social-media-list">
  <li><a href="https://github.com/sel4"><i class="fab fa-github"></i> <span class="username">sel4</span></a></li><li><a href="https://github.com/sel4proj"><i class="fab fa-github"></i> <span class="username">sel4proj</span></a></li>
</ul>

    </div>

    <div class="col-md-8">
      <ul class="list-unstyled">
        <li>
          This site is for displaying seL4 related documentation.  Pull requests are welcome.
        </li>
        
          <li>
            Site last updated: Fri Feb 7 10:17:38 2025 +1100 ee78c8857c
          </li>
          <li>
                Page last updated: Tue Jan 14 15:56:06 2025 +1100 f28f1dfa66
          </li>
        
      </ul>
    </div>
    <div class="col-md-2">
<a href="https://github.com/seL4/docs/blob/master/projects/sel4/verified-configurations.md">View page on GitHub</a>
      <br />
      <a href="https://github.com/seL4/docs/edit/master/projects/sel4/verified-configurations.md">Edit page on GitHub</a>
      <br />
      <a href="/sitemap">Sitemap</a>
    </div>

  </div>

</footer>

  </body>
</html>
